#include "stdafx.h"
#include "ExpliSatConverter.h"
#include "formal.h"

ExpliSatConverter::ExpliSatConverter()
{
}


ExpliSatConverter::~ExpliSatConverter()
{
}


Attack* ExpliSatConverter::CreateAttractionAttack(Topology* pTopology, As* pVictim, As* pAttacker)
{
	BgpMessage* msg = CreateAttractionAttackMsg(pTopology, pVictim, pAttacker);
	Set<As*>* whoSendTo = CreateAttractionAttackWhoToSendTo(msg, pVictim, pAttacker);
	return new 	Attack(msg, whoSendTo);
}


// pSizeOfPath - first create small size paths, and then longer and longer
BgpMessage* ExpliSatConverter::CreateAttractionAttackMsg(Topology* pTopology, As* pVictim, As* pAttacker)
{
	Map<As*, Vector<As*> >* pathToVictim = new Map<As*, Vector<As*> >();
	Vector<As*>* path = CreatePathToPublish(pTopology);
	path->push_back(pVictim);
	(*pathToVictim)[pVictim] = (*path);

	return new BgpMessage(pathToVictim);
}

Set<As*>* ExpliSatConverter::CreateAttractionAttackWhoToSendTo(BgpMessage* pMsg, As* pVictim, As* pAttacker)
{
	// return all neighbors except the first hop
	Set<Vertex*>* neighbors = new Set<Vertex*>();
	pAttacker->GetNeighbors(neighbors);

	Map<As*, Vector<As*> >::iterator itVictim = pMsg->UpdatedPaths->find(pVictim);
	As* victimFirstHop = itVictim == pMsg->UpdatedPaths->end() ? 0 : pMsg->UpdatedPaths->at(pVictim).front();

	//Set<Vertex*>::iterator itNeighbors = neighbors->find(victimFirstHop);
	Set<Vertex*>::iterator itNeighbors = neighbors->find(neighbors->begin(), neighbors->end(), victimFirstHop);
	neighbors->erase(itNeighbors);

	Set<As*>* result = reinterpret_cast<Set<As*>*>(neighbors);
	return result;
}

Vector<As*>* ExpliSatConverter::CreatePathToPublish(Topology* pTopology)
{
	// AS0 = The Attacker
	// AS1= The Victim
	Vector<As*>* resultPath = new Vector<As*>();
	Vector<As*>* ass = pTopology->GetOrderedAssAfterInitialized();
	int topologySize = ass->size();

	int sizeOfPath = 4; // TODO - fv_non_det_int with assumes from 0 till topologySize - 2
	//unsigned int sizeOfPath = nondet_uint(); // TODO - fv_non_det_int with assumes from 0 till topologySize - 2


	unsigned int asNum = nondet_uint();
	fv_assume(asNum > 1);
	fv_assume(asNum <= topologySize);
	int previousAsNumber = asNum;
	for (int asNumIndex = 0; asNumIndex < sizeOfPath; ++asNumIndex)
	{
		if (asNum == topologySize)
		{
			break;
		}
		resultPath->push_back((*ass)[asNum]);
		previousAsNumber = asNum;
		asNum = nondet_uint();
		fv_assume(asNum > 1);
		fv_assume(asNum <= topologySize);

	}
	return resultPath;
}



//#include <iostream>
// Algorithm to recursively search network for paths
void ExpliSatConverter::DepthFirst(Topology* network, Vector<Vertex*>& visited, Vertex* end, Vector<Vector<As*>*>* dfsPaths)
{
	//Vector<Vector<As*>*>* dfsPaths = new Vector<Vector<As*>*>();

	Vertex* back = visited.back();
	Set<Vertex*>* adjNode = new Set<Vertex*>();
	back->GetNeighbors(adjNode);

	// Examine adjacent nodes
	for (Set<Vertex*>::iterator node_it = adjNode->begin();	node_it != adjNode->end(); node_it++)
	{
		Vertex* node = (*node_it);
		
		if (visited.find(node) != visited.end()) continue;

		if (node->_name == end->_name)
		{
			visited.push_back(*node_it);

			int hops = (int)visited.size();
			Vector<As*>* dfsPath = new Vector<As*>();
			for (int i = 0; i < hops; i++)
			{
				dfsPath->push_back((As*)visited[i]);
				//std::cout << visited[i]->_name << " ";
			}
			dfsPaths->push_back(dfsPath);
			//std::cout << std::endl;

			int n = (int)visited.size() - 1;
			visited.erase(visited.begin() + n);

			break;
		}
	}

	// in breadth-first, recursion needs to come after visiting adjacent nodes
	for (Vector<Vertex*>::iterator node_it = adjNode->begin();
		node_it != adjNode->end();
		node_it++)
	{
		Vertex* node = (*node_it);

		if ((visited.find(node) != visited.end()) || node->_name == end->_name)
			continue;

		visited.push_back(node);

		DepthFirst(network, visited, end, dfsPaths);

		int n = (int)visited.size() - 1;
		visited.erase(visited.begin() + n);
	}
	//return dfsPaths;
}

Attack* ExpliSatConverter::CreateInterceptionAttack(Topology* pTopology, As* pVictim, As* pAttacker)
{
	BgpMessage* msg = CreateInterceptionAttackMsg(pTopology, pVictim, pAttacker);
	Set<As*>* whoSendTo = CreateAttractionAttackWhoToSendTo(msg, pVictim, pAttacker);
	return new 	Attack(msg, whoSendTo);
}

// pSizeOfPath - first create small size paths, and then longer and longer
BgpMessage* ExpliSatConverter::CreateInterceptionAttackMsg(Topology* pTopology, As* pVictim, As* pAttacker)
{
	Map<As*, Vector<As*> >* pathToVictim = new Map<As*, Vector<As*> >();

	Vector<Vertex*> visited;
	visited.push_back(pAttacker);
	Vector<Vector<As*>*>* dfsPaths = new Vector<Vector<As*>*>();
	DepthFirst(pTopology, visited, pVictim, dfsPaths);
	unsigned int dfsPathNumber = nondet_uint();
	fv_assume(dfsPathNumber < dfsPaths->size());

	Vector<As*>* path = dfsPaths->at(dfsPathNumber);
	path->erase(path->begin());
	(*pathToVictim)[pVictim] = (*path);

	return new BgpMessage(pathToVictim);
}


// pVictim and pAttacker are already created (out if this function scope)
Topology* ExpliSatConverter::CreateTopology(As* pVictim, AttackerAs* pAttacker)
{
	Topology* g = new Topology();
	Vector<As*>* orderedAss = new Vector<As*>();

	unsigned int topologySize = 10;  // TODO - non_det and assume < 5 (to begin with), then grow for more
	//unsigned int topologySize = nondet_uint();
	//fv_assume(topologySize > 3);	
	//fv_assume(topologySize < 5);	
	//  Prepare Vertices
	// fill the order of the ass's (does not matter, all it matter is for the attacker and the victim will be first)
	orderedAss->push_back(pAttacker);
	orderedAss->push_back(pVictim);
	for (unsigned int asNum = 2; asNum < topologySize + 2; asNum++)
	{
		orderedAss->push_back(new As(asNum));
	}
	As* firstAs = 0;
	As* secondAs = 0;
	unsigned char relation = 0;
	int notImportant = -1;
	//  Prepare Edges
	for (unsigned int firstAsIndex = 2; firstAsIndex < orderedAss->size() - 1; firstAsIndex++)
	{
		for (unsigned int secondAsIndex = firstAsIndex + 1; secondAsIndex < orderedAss->size(); secondAsIndex++)
		{
			firstAs = orderedAss->at(firstAsIndex);
			secondAs = orderedAss->at(secondAsIndex);
			relation = nondet_uchar(); // TODO - non_det and assume 0 <= x <= 2
			fv_assume(relation >= 0);
			fv_assume(relation <= 3);
			if (relation == 0)
			{
				g->InsertCustomerProvider(firstAs, secondAs);
			}
			else if (relation == 1)
			{
				g->InsertCustomerProvider(secondAs, firstAs);
			}
			else if (relation == 2)
			{
				g->InsertPeerToPeer(firstAs, secondAs);
			}
			//else
			//{
			//	// no relation
			//}

			//notImportant = (relation == 0) ? g->InsertCustomerProvider(firstAs, secondAs) :
			//	((relation == 1) ? g->InsertPeerToPeer(firstAs, secondAs) : 2);
		}
	}

	g->InitializeOrderedAss(orderedAss);
	return g;
}




